J. Alt, S. Artemov; "Reflective λ-Calculus"
Memo
Jesse Alt
,
Sergei N. Artemov
https://link.springer.com/chapter/10.1007/3-540-45504-3_2
Abstrakt
$ λ^\infty
という
型付きλ計算
の体系について．
「証明の証明」の証明
といったモノを扱ったり出来るようになる？